SherbyNet - /page/wikibook/entry.mu

Micron Document

<!DOCTYPE html>

<title>SPARK (programming language)</title>

</head>

<span id="openzim-page-title" class="mw-page-title-main"><span class="mw-page-title-main">SPARK (programming language)</span></span>

</h1>

</header>

/* start https://en.wikipedia.org/ */

.mw-parser-output .hatnote{font-style:italic}.mw-parser-output div.hatnote{padding-left:1.6em;margin-bottom:0.5em}.mw-parser-output .hatnote i{font-style:normal}.mw-parser-output .hatnote+link+.hatnote{margin-top:-0.5em}@media print{body.ns-0 .mw-parser-output .hatnote{display:none!important}}

/* end https://en.wikipedia.org/ */

</style><div role="note" class="hatnote navigation-not-searchable">This article is about the <a href="Programming_language" title="Programming language">programming language</a>. For the <a href="Cluster_computing" class="mw-redirect" title="Cluster computing">cluster computing</a> framework that can run on <a href="Scala_(programming_language)" title="Scala (programming language)">Scala</a>, <a href="Java_(programming_language)" title="Java (programming language)">Java</a>, and <a href="Python_(programming_language)" title="Python (programming language)">Python</a>, see <a href="Apache_Spark" title="Apache Spark">Apache Spark</a>.</div>

</p>

/* start https://en.wikipedia.org/ */

.mw-parser-output .ambox{border:1px solid #a2a9b1;border-left:10px solid #36c;background-color:#fbfbfb;box-sizing:border-box}.mw-parser-output .ambox+link+.ambox,.mw-parser-output .ambox+link+style+.ambox,.mw-parser-output .ambox+link+link+.ambox,.mw-parser-output .ambox+.mw-empty-elt+link+.ambox,.mw-parser-output .ambox+.mw-empty-elt+link+style+.ambox,.mw-parser-output .ambox+.mw-empty-elt+link+link+.ambox{margin-top:-1px}html body.mediawiki .mw-parser-output .ambox.mbox-small-left{margin:4px 1em 4px 0;overflow:hidden;width:238px;border-collapse:collapse;font-size:88%;line-height:1.25em}.mw-parser-output .ambox-speedy{border-left:10px solid #b32424;background-color:#fee7e6}.mw-parser-output .ambox-delete{border-left:10px solid #b32424}.mw-parser-output .ambox-content{border-left:10px solid #f28500}.mw-parser-output .ambox-style{border-left:10px solid #fc3}.mw-parser-output .ambox-move{border-left:10px solid #9932cc}.mw-parser-output .ambox-protection{border-left:10px solid #a2a9b1}.mw-parser-output .ambox .mbox-text{border:none;padding:0.25em 0.5em;width:100%}.mw-parser-output .ambox .mbox-image{border:none;padding:2px 0 2px 0.5em;text-align:center}.mw-parser-output .ambox .mbox-imageright{border:none;padding:2px 0.5em 2px 0;text-align:center}.mw-parser-output .ambox .mbox-empty-cell{border:none;padding:0;width:1px}.mw-parser-output .ambox .mbox-image-div{width:52px}@media(min-width:720px){.mw-parser-output .ambox{margin:0 10%}}@media print{body.ns-0 .mw-parser-output .ambox{display:none!important}}

/* end https://en.wikipedia.org/ */

</style><style data-mw-deduplicate="TemplateStyles:r1248332772">

/* start https://en.wikipedia.org/ */

.mw-parser-output .multiple-issues-text{width:95%;margin:0.2em 0}.mw-parser-output .multiple-issues-text>.mw-collapsible-content{margin-top:0.3em}.mw-parser-output .compact-ambox .ambox{border:none;border-collapse:collapse;background-color:transparent;margin:0 0 0 1.6em!important;padding:0!important;width:auto;display:block}body.mediawiki .mw-parser-output .compact-ambox .ambox.mbox-small-left{font-size:100%;width:auto;margin:0}.mw-parser-output .compact-ambox .ambox .mbox-text{padding:0!important;margin:0!important}.mw-parser-output .compact-ambox .ambox .mbox-text-span{display:list-item;line-height:1.5em;list-style-type:disc}body.skin-minerva .mw-parser-output .multiple-issues-text>.mw-collapsible-toggle,.mw-parser-output .compact-ambox .ambox .mbox-image,.mw-parser-output .compact-ambox .ambox .mbox-imageright,.mw-parser-output .compact-ambox .ambox .mbox-empty-cell,.mw-parser-output .compact-ambox .hide-when-compact{display:none}

/* end https://en.wikipedia.org/ */

</style>

/* start https://en.wikipedia.org/ */

.mw-parser-output .infobox-subbox{padding:0;border:none;margin:-3px;width:auto;min-width:100%;font-size:100%;clear:none;float:none;background-color:transparent}.mw-parser-output .infobox-3cols-child{margin:auto}.mw-parser-output .infobox .navbar{font-size:100%}@media screen{html.skin-theme-clientpref-night .mw-parser-output .infobox-full-data:not(.notheme)>div:not(.notheme)[style]{background:#1f1f23!important;color:#f8f9fa}}@media screen and (prefers-color-scheme:dark){html.skin-theme-clientpref-os .mw-parser-output .infobox-full-data:not(.notheme)>div:not(.notheme)[style]{background:#1f1f23!important;color:#f8f9fa}}@media(min-width:640px){body.skin--responsive .mw-parser-output .infobox-table{display:table!important}body.skin--responsive .mw-parser-output .infobox-table>caption{display:table-caption!important}body.skin--responsive .mw-parser-output .infobox-table>tbody{display:table-row-group}body.skin--responsive .mw-parser-output .infobox-table th,body.skin--responsive .mw-parser-output .infobox-table td{padding-left:inherit;padding-right:inherit}}

/* end https://en.wikipedia.org/ */

</style><table class="infobox vevent"><tbody><tr><th colspan="2" class="infobox-above" style="background-color:#e0e0e0;">SPARK</th></tr><tr><td colspan="2" class="infobox-image"><span typeof="mw:File"></span></td></tr><tr><th scope="row" class="infobox-label"><a href="Programming_paradigm" title="Programming paradigm">Paradigm</a></th><td class="infobox-data"><a href="Multi-paradigm_programming_language" class="mw-redirect" title="Multi-paradigm programming language">Multi-paradigm</a>: <a href="Structured_programming" title="Structured programming">structured</a>, <a href="Imperative_programming" title="Imperative programming">imperative</a>, <a href="Object-oriented_programming" title="Object-oriented programming">object-oriented</a>, <a href="Aspect-oriented_programming" title="Aspect-oriented programming">aspect-oriented</a>,<sup id="cite_ref-1" class="reference"><a href="#cite_note-1"><span class="cite-bracket">[</span>1<span class="cite-bracket">]</span></a></sup> <a href="Concurrent_programming" class="mw-redirect" title="Concurrent programming">concurrent</a>, <a href="Array_programming" title="Array programming">array</a>, <a href="Distributed_computing" title="Distributed computing">distributed</a>, <a href="Generic_programming" title="Generic programming">generic</a>, <a href="Procedural_programming" title="Procedural programming">procedural</a>, <a href="Metaprogramming" title="Metaprogramming">meta</a></td></tr><tr><th scope="row" class="infobox-label">Family</th><td class="infobox-data"><a href="Ada_(programming_language)" title="Ada (programming language)">Ada</a></td></tr><tr><th scope="row" class="infobox-label"><a href="Software_developer" class="mw-redirect" title="Software developer">Developer</a></th><td class="infobox-data organiser"><a href="Altran" class="mw-redirect" title="Altran">Altran</a>, <a href="AdaCore" class="mw-redirect" title="AdaCore">AdaCore</a></td></tr><tr><th scope="row" class="infobox-label">First appeared</th><td class="infobox-data">2009<span style="display:none"> (<span class="bday dtstart published updated">2009</span>)</span></td></tr><tr><td colspan="2" class="infobox-full-data"></td></tr><tr><th scope="row" class="infobox-label" style="white-space: nowrap;"><a href="Software_release_life_cycle" title="Software release life cycle">Stable release</a></th><td class="infobox-data"><div style="margin:0px;">Community 2021

/ June 1, 2021<span style="display:none"> (<span class="bday dtstart published updated">2021-06-01</span>)</span></div></td></tr><tr style="display:none"><td colspan="2">

</td></tr><tr><th scope="row" class="infobox-label"><a href="Type_system" title="Type system">Typing discipline</a></th><td class="infobox-data"><a href="Static_typing" class="mw-redirect" title="Static typing">static</a>, <a href="Strong_and_weak_typing" title="Strong and weak typing">strong</a>, <a href="Type_safety" title="Type safety">safe</a>, <a href="Nominative_type_system" class="mw-redirect" title="Nominative type system">nominative</a></td></tr><tr><th scope="row" class="infobox-label"><a href="Operating_system" title="Operating system">OS</a></th><td class="infobox-data"><a href="Cross-platform" class="mw-redirect" title="Cross-platform">Cross-platform</a>: <a href="Linux" title="Linux">Linux</a>, <a href="Microsoft_Windows" title="Microsoft Windows">Windows</a>, <a href="MacOS" title="MacOS">macOS</a></td></tr><tr><th scope="row" class="infobox-label"><a href="Software_license" title="Software license">License</a></th><td class="infobox-data"><a href="GNU_General_Public_License" title="GNU General Public License">GPLv3</a></td></tr><tr><th scope="row" class="infobox-label">Website</th><td class="infobox-data"><span class="url"><a rel="nofollow" class="external text" href="http://www.adacore.com/about-spark">www<wbr>.adacore<wbr>.com<wbr>/about-spark</a></span></td></tr><tr><th colspan="2" class="infobox-header" style="background-color: #EEEEEE;">Major <a href="Programming_language_implementation" title="Programming language implementation">implementations</a></th></tr><tr><td colspan="2" class="infobox-full-data">SPARK Pro, SPARK GPL Edition, SPARK Community</td></tr><tr><th colspan="2" class="infobox-header" style="background-color: #EEEEEE;">Influenced by</th></tr><tr><td colspan="2" class="infobox-full-data"><a href="Ada_(programming_language)" title="Ada (programming language)">Ada</a>, <a href="Eiffel_(programming_language)" title="Eiffel (programming language)">Eiffel</a></td></tr></tbody></table>

<p><b>SPARK</b> is a <a href="Formal_semantics_of_programming_languages" class="mw-redirect" title="Formal semantics of programming languages">formally defined</a> <a href="Computer" title="Computer">computer</a> <a href="Programming_language" title="Programming language">programming language</a> based on the <a href="Ada_(programming_language)" title="Ada (programming language)">Ada</a> language, intended for developing <a href="High_integrity_software" class="mw-redirect" title="High integrity software">high integrity software</a> used in systems where predictable and highly reliable operation is essential. It facilitates developing applications that demand safety, security, or business integrity.

</p><p>Originally, three versions of SPARK existed (SPARK83, SPARK95, SPARK2005), based on Ada 83, Ada 95, and Ada 2005 respectively.

</p><p>A fourth version, SPARK 2014, based on Ada 2012, was released on April 30, 2014. SPARK 2014 is a complete re-design of the language and supporting <a href="Software_verification" title="Software verification">verification</a> tools.

</p><p>The SPARK language consists of a well-defined subset of the Ada language that uses <a href="Design_by_contract" title="Design by contract">contracts</a> to describe the specification of components in a form that is suitable for both static and dynamic verification.

</p><p>In SPARK83/95/2005, the contracts are encoded in Ada comments and so are ignored by any standard Ada compiler, but are processed by the SPARK <i>Examiner</i> and its associated tools.

</p><p>SPARK 2014, in contrast, uses Ada 2012's built-in <a href="Syntax_(programming_languages)" title="Syntax (programming languages)">syntax</a> of <i><a href="Aspect-oriented_programming" title="Aspect-oriented programming">aspects</a></i> to express contracts, bringing them into the core of the language. The main tool for SPARK 2014 (GNATprove) is based on the <a href="GNAT" title="GNAT">GNAT/GCC</a> infrastructure, and re-uses almost all of the GNAT Ada 2012 front-end.

</p>

<div class="mw-heading mw-heading2"><h2 id="Technical_overview">Technical overview</h2></div>

<p>SPARK utilises the strengths of Ada while trying to eliminate all its potential ambiguities and insecure constructs. SPARK programs are by design meant to be unambiguous, and their behavior is required to be unaffected by the choice of Ada <a href="Compiler" title="Compiler">compiler</a>. These goals are achieved partly by omitting some of Ada's more problematic features (such as unrestricted <a href="Task_parallelism" title="Task parallelism">parallel tasking</a>) and partly by introducing contracts that encode the application designer's intentions and requirements for certain components of a program.

</p><p>The combination of these approaches allows SPARK to meet its design objectives, which are:

</p>

<ul><li>logical <a href="Soundness" title="Soundness">soundness</a></li>

<li>rigorous formal definition</li>

<li>simple semantics</li>

<li>security</li>

<li><a href="Expressive_power_(computer_science)" title="Expressive power (computer science)">expressive power</a></li>

<li><a href="Verification_and_validation" title="Verification and validation">verifiability</a></li>

<li>bounded resource (space and time) requirements.</li>

<li>minimal runtime system requirements</li></ul>

<div class="mw-heading mw-heading2"><h2 id="Contract_examples">Contract examples</h2></div>

<p>Consider the Ada subprogram specification below:

</p>

<pre><b>procedure</b> Increment (X : <b>in out</b> Counter_Type);

</pre>

<p>In pure Ada, this might increment the variable <code>X</code> by one or one thousand; or it might set some global counter to <code>X</code> and return the original value of the counter in <code>X</code>; or it might do nothing with <code>X</code>.

</p><p>With SPARK 2014, contracts are added to the code to provide more information regarding what a subprogram actually does. For example, the above specification may be altered to say:

</p>

<pre><b>procedure</b> Increment (X : <b>in out</b> Counter_Type)

<b> with</b> Global => <b>null</b>,

Depends => (X => X);

</pre>

<p>This specifies that the <code>Increment</code> procedure uses no (neither update nor read) global variable and that the only data item used in calculating the new value of <code>X</code> is <code>X</code> alone.

</p><p>Alternatively, may be specified:

</p>

<pre><b>procedure</b> Increment (X : <b>in out</b> Counter_Type)

<b> with</b> Global => (In_Out => Count),

Depends => (Count => (Count, X),

X => null);

</pre>

<p>This specifies that <code>Increment</code> will use the global variable <code>Count</code> in the same package as <code>Increment</code>, that the exported value of <code>Count</code> depends on the imported values of <code>Count</code> and <code>X</code>, and that the exported value of <code>X</code> does not depend on any variables at all and it will be derived from constant data only.

</p><p>If GNATprove is then run on the specification and corresponding body of a subprogram, it will analyse the body of the subprogram to build up a model of the information flow. This model is then compared against what has been specified by the annotations and any discrepancies reported to the user.

</p><p>These specifications can be further extended by asserting various properties that either need to hold when a subprogram is called (<i><a href="Precondition" title="Precondition">preconditions</a></i>) or that will hold once execution of the subprogram has completed (<i><a href="Postcondition" title="Postcondition">postconditions</a></i>). For example, if writing:

</p>

<pre><b>procedure</b> Increment (X : <b>in out</b> Counter_Type)

<b> with</b> Global => null,

Depends => (X => X),

Pre => X < Counter_Type'Last,

Post => X = X'Old + 1;

</pre>

<p>This, now, specifies not only that <code>X</code> is derived from itself alone, but also that before <code>Increment</code> is called <code>X</code> must be strictly less than the last possible value of its type (to ensure that the result will never <a href="Integer_overflow" title="Integer overflow">overflow</a>) and that afterward <code>X</code> will be equal to the initial value of <code>X</code> plus one.

</p>

<div class="mw-heading mw-heading2"><h2 id="Verification_conditions">Verification conditions</h2></div>

<p>GNATprove can also generate a set of <a href="Verification_condition_generator" title="Verification condition generator">verification conditions</a> (VCs). These are used to establish whether certain properties hold for a given subprogram. At a minimum, the GNATprove will generate VCs to establish that all run-time errors cannot occur within a subprogram, such as:

</p>

<ul><li>array index out of range</li>

<li>type range violation</li>

<li>division by zero</li>

<li>numerical overflow</li></ul>

<p>If a postcondition or any other assertion is added to a subprogram, GNATprove will also generate VCs that require the user to show that these properties hold for all possible paths through the subprogram.

</p><p>Under the hood, GNATprove uses the Why3 intermediate language and VC Generator, and the <a href="CVC4" class="mw-redirect" title="CVC4">CVC4</a>, <a href="Z3_Theorem_Prover" title="Z3 Theorem Prover">Z3</a>, and <a href="Alt-Ergo" title="Alt-Ergo">Alt-Ergo</a> theorem provers to discharge VCs. Use of other provers (including interactive proof checkers) is also possible through other components of the Why3 toolset.

</p>

<div class="mw-heading mw-heading2"><h2 id="History">History</h2></div>

<p>The first version of SPARK (based on Ada 83) was produced at the <a href="University_of_Southampton" title="University of Southampton">University of Southampton</a> (with UK <a href="Ministry_of_Defence_(United_Kingdom)" title="Ministry of Defence (United Kingdom)">Ministry of Defence</a> sponsorship) by Bernard Carré and Trevor Jennings. The name <i>SPARK</i> was derived from <i>SPADE Ada Kernel</i>, in reference to the <i>SPADE</i> subset of the <a href="Pascal_programming_language" class="mw-redirect" title="Pascal programming language">Pascal programming language</a>.<sup id="cite_ref-spark_lang_ref_manual_2-0" class="reference"><a href="#cite_note-spark_lang_ref_manual-2"><span class="cite-bracket">[</span>2<span class="cite-bracket">]</span></a></sup>

</p><p>Subsequently the language was progressively extended and refined, first by Program Validation Limited and then by Praxis Critical Systems Limited. In 2004, Praxis Critical Systems Limited changed its name to Praxis High Integrity Systems Limited. In January 2010, the company became <a href="Altran_Praxis" title="Altran Praxis">Altran Praxis</a>.

</p><p>In early 2009, Praxis formed a partnership with AdaCore, and released <i>SPARK Pro</i> under the terms of the GPL. This was followed in June 2009 by the SPARK GPL Edition 2009, aimed at the <a href="Free_and_open-source_software" title="Free and open-source software">free and open-source software</a> (FOSS) and academic communities.

</p><p>In June 2010, Altran-Praxis announced that the SPARK programming language would be used in the software of US Lunar project <i><a href="Lunar_IceCube" title="Lunar IceCube">CubeSat</a></i>, expected to be completed in 2015.

</p><p>In January 2013, Altran-Praxis changed its name to Altran, which in April 2021 became <a href="Capgemini_Engineering" title="Capgemini Engineering">Capgemini Engineering</a> (following Altran's merger with <a href="Capgemini" title="Capgemini">Capgemini</a>).

</p><p>The first Pro release of SPARK 2014 was announced on April 30, 2014, and was quickly followed by the SPARK 2014 GPL edition, aimed at the <a href="FLOSS" class="mw-redirect" title="FLOSS">FLOSS</a> and academic communities.

</p>

<div class="mw-heading mw-heading2"><h2 id="Industrial_applications">Industrial applications</h2></div>

<div class="mw-heading mw-heading3"><h3 id="Safety-related_systems">Safety-related systems</h3></div>

<p>SPARK has been used in several high profile safety-critical systems, covering commercial aviation (<a href="Rolls-Royce_Trent" title="Rolls-Royce Trent">Rolls-Royce Trent</a> series jet engines, the ARINC ACAMS system, the <a href="Lockheed_Martin_C-130J_Super_Hercules" title="Lockheed Martin C-130J Super Hercules">Lockheed Martin C130J</a>), military aviation (<a href="Eurofighter_Typhoon" title="Eurofighter Typhoon">EuroFighter Typhoon</a>, <a href="Harrier_GR9" class="mw-redirect" title="Harrier GR9">Harrier GR9</a>, <a href="Aermacchi_M-346" class="mw-redirect" title="Aermacchi M-346">AerMacchi M346</a>), air-traffic management (UK NATS iFACTS system), rail (numerous signalling applications), medical (the LifeFlow <a href="Ventricular_assist_device" title="Ventricular assist device">ventricular assist device</a>), and space applications (the <a href="Vermont_Lunar_CubeSat" title="Vermont Lunar CubeSat">Vermont Technical College CubeSat project</a>).

</p>

<div class="mw-heading mw-heading3"><h3 id="Security-related_systems">Security-related systems</h3></div>

<p>SPARK has also been used in secure systems development. Users include <a href="Rockwell_Collins" title="Rockwell Collins">Rockwell Collins</a> (Turnstile and SecureOne cross-domain solutions), the development of the original <a href="MULTOS" title="MULTOS">MULTOS</a> CA, the NSA Tokeneer demonstrator, the secunet multi-level workstation, the Muen separation kernel and <a href="Genode" title="Genode">Genode</a> block-device encrypter.

</p><p>In August 2010, Rod Chapman, principal engineer of Altran Praxis, implemented <a href="Skein_(hash_function)" title="Skein (hash function)">Skein</a>, one of candidates for <a href="Sha-3" class="mw-redirect" title="Sha-3">SHA-3</a>, in SPARK. In comparing the performance of the SPARK and C implementations and after careful optimization, he managed to have the SPARK version run only about 5 to 10% slower than C. Later improvement to the Ada middle-end in GCC (implemented by Eric Botcazou of AdaCore) closed the gap, with the SPARK code matching the C in performance exactly.<sup id="cite_ref-3" class="reference"><a href="#cite_note-3"><span class="cite-bracket">[</span>3<span class="cite-bracket">]</span></a></sup>

</p><p>NVIDIA have also adopted SPARK for the implementation of security-critical firmware.<sup id="cite_ref-4" class="reference"><a href="#cite_note-4"><span class="cite-bracket">[</span>4<span class="cite-bracket">]</span></a></sup><sup id="cite_ref-5" class="reference"><a href="#cite_note-5"><span class="cite-bracket">[</span>5<span class="cite-bracket">]</span></a></sup>

</p><p>In 2020, Rod Chapman re-implemented the TweetNaCl cryptographic library in SPARK 2014.<sup id="cite_ref-6" class="reference"><a href="#cite_note-6"><span class="cite-bracket">[</span>6<span class="cite-bracket">]</span></a></sup> The SPARK version of the library has a complete auto-active proof of type-safety, memory-safety and some correctness properties, and retains constant-time algorithms throughout. The SPARK code is also significantly faster than TweetNaCl.

</p>

/* start https://en.wikipedia.org/ */

.mw-parser-output .portalbox{padding:0;margin:0.5em 0;display:table;box-sizing:border-box;max-width:175px;list-style:none}.mw-parser-output .portalborder{border:1px solid var(--border-color-base,#a2a9b1);padding:0.1em;background:var(--background-color-neutral-subtle,#f8f9fa)}.mw-parser-output .portalbox-entry{display:table-row;font-size:85%;line-height:110%;height:1.9em;font-style:italic;font-weight:bold}.mw-parser-output .portalbox-image{display:table-cell;padding:0.2em;vertical-align:middle;text-align:center}.mw-parser-output .portalbox-link{display:table-cell;padding:0.2em 0.2em 0.2em 0.3em;vertical-align:middle}@media(min-width:720px){.mw-parser-output .portalleft{margin:0.5em 1em 0.5em 0}.mw-parser-output .portalright{clear:right;float:right;margin:0.5em 0 0.5em 1em}}

/* end https://en.wikipedia.org/ */

</style>

<ul><li><a href="Z_notation" title="Z notation">Z notation</a></li>

<li><a href="Java_Modeling_Language" title="Java Modeling Language">Java Modeling Language</a></li></ul>

<div class="mw-heading mw-heading2"><h2 id="References">References</h2></div>

/* start https://en.wikipedia.org/ */

.mw-parser-output .reflist{margin-bottom:0.5em;list-style-type:decimal}@media screen{.mw-parser-output .reflist{font-size:90%}}.mw-parser-output .reflist .references{font-size:100%;margin-bottom:0;list-style-type:inherit}.mw-parser-output .reflist-columns-2{column-width:30em}.mw-parser-output .reflist-columns-3{column-width:25em}.mw-parser-output .reflist-columns{margin-top:0.3em}.mw-parser-output .reflist-columns ol{margin-top:0}.mw-parser-output .reflist-columns li{page-break-inside:avoid;break-inside:avoid-column}.mw-parser-output .reflist-upper-alpha{list-style-type:upper-alpha}.mw-parser-output .reflist-upper-roman{list-style-type:upper-roman}.mw-parser-output .reflist-lower-alpha{list-style-type:lower-alpha}.mw-parser-output .reflist-lower-greek{list-style-type:lower-greek}.mw-parser-output .reflist-lower-roman{list-style-type:lower-roman}

/* end https://en.wikipedia.org/ */

</style><div class="reflist">

/* start https://en.wikipedia.org/ */

.mw-parser-output cite.citation{font-style:inherit;word-wrap:break-word}.mw-parser-output .citation q{quotes:"\"""\"""'""'"}.mw-parser-output .citation:target{background-color:rgba(0,127,255,0.133)}.mw-parser-output .id-lock-free.id-lock-free a{background:url("./mw/Lock-green.svg")right 0.1em center/9px no-repeat}.mw-parser-output .id-lock-limited.id-lock-limited a,.mw-parser-output .id-lock-registration.id-lock-registration a{background:url("./mw/Lock-gray-alt-2.svg")right 0.1em center/9px no-repeat}.mw-parser-output .id-lock-subscription.id-lock-subscription a{background:url("./mw/Lock-red-alt-2.svg")right 0.1em center/9px no-repeat}.mw-parser-output .cs1-ws-icon a{background:url("./mw/Wikisource-logo.svg")right 0.1em center/12px no-repeat}body:not(.skin-timeless):not(.skin-minerva) .mw-parser-output .id-lock-free a,body:not(.skin-timeless):not(.skin-minerva) .mw-parser-output .id-lock-limited a,body:not(.skin-timeless):not(.skin-minerva) .mw-parser-output .id-lock-registration a,body:not(.skin-timeless):not(.skin-minerva) .mw-parser-output .id-lock-subscription a,body:not(.skin-timeless):not(.skin-minerva) .mw-parser-output .cs1-ws-icon a{background-size:contain;padding:0 1em 0 0}.mw-parser-output .cs1-code{color:inherit;background:inherit;border:none;padding:inherit}.mw-parser-output .cs1-hidden-error{display:none;color:var(--color-error,#d33)}.mw-parser-output .cs1-visible-error{color:var(--color-error,#d33)}.mw-parser-output .cs1-maint{display:none;color:#085;margin-left:0.3em}.mw-parser-output .cs1-kern-left{padding-left:0.2em}.mw-parser-output .cs1-kern-right{padding-right:0.2em}.mw-parser-output .citation .mw-selflink{font-weight:inherit}@media screen{.mw-parser-output .cs1-format{font-size:95%}html.skin-theme-clientpref-night .mw-parser-output .cs1-maint{color:#18911f}}@media screen and (prefers-color-scheme:dark){html.skin-theme-clientpref-os .mw-parser-output .cs1-maint{color:#18911f}}

/* end https://en.wikipedia.org/ */

</style><cite class="citation web cs1"><a rel="nofollow" class="external text" href="http://www.adacore.com/uploads/technical-papers/Ada2012_Rational_Introducion.pdf">"Ada2012 Rationale"</a> <span class="cs1-format">(PDF)</span>. <i>adacore.com</i>. <a rel="nofollow" class="external text" href="https://web.archive.org/web/20160418132340/http://www.adacore.com/uploads/technical-papers/Ada2012_Rational_Introducion.pdf">Archived</a> <span class="cs1-format">(PDF)</span> from the original on 18 April 2016<span class="reference-accessdate">. Retrieved <span class="nowrap">5 May</span> 2018</span>.</cite></span>

</li>

<li id="cite_note-spark_lang_ref_manual-2"><span class="mw-cite-backlink"><b><a href="#cite_ref-spark_lang_ref_manual_2-0">^</a></b></span> <span class="reference-text"><cite class="citation web cs1"><a rel="nofollow" class="external text" href="https://docs.adacore.com/sparkdocs-docs/SPARK_LRM.htm">"SPARK – The SPADE Ada Kernel (including RavenSPARK)"</a>. AdaCore<span class="reference-accessdate">. Retrieved <span class="nowrap">30 June</span> 2021</span>.</cite></span>

</li>

<li id="cite_note-3"><span class="mw-cite-backlink"><b><a href="#cite_ref-3">^</a></b></span> <span class="reference-text"><cite id="CITEREFHandy2010" class="citation news cs1">Handy, Alex (24 August 2010). <a rel="nofollow" class="external text" href="http://www.sdtimes.com/link/34579">"Ada-derived Skein crypto shows SPARK"</a>. <i><a href="SD_Times" title="SD Times">SD Times</a></i>. BZ Media LLC<span class="reference-accessdate">. Retrieved <span class="nowrap">31 August</span> 2010</span>.</cite></span>

</li>

<li id="cite_note-4"><span class="mw-cite-backlink"><b><a href="#cite_ref-4">^</a></b></span> <span class="reference-text"><cite class="citation web cs1"><a rel="nofollow" class="external text" href="https://www.slideshare.net/AdaCore/securing-the-future-of-safety-and-security-of-embedded-software">"Securing the Future of Safety and Security of Embedded Software"</a>. 8 January 2020.</cite></span>

</li>

<li id="cite_note-5"><span class="mw-cite-backlink"><b><a href="#cite_ref-5">^</a></b></span> <span class="reference-text"><cite id="CITEREFZabrockiMitic2025" class="citation web cs1">Zabrocki, Adam; Mitic, Marko (8 August 2025). <a rel="nofollow" class="external text" href="https://media.defcon.org/DEF%20CON%2033/DEF%20CON%2033%20presentations/Adam%20Zabrocki%20Marko%20Mitic%20-%20How%20to%20secure%20unique%20ecosystem%20shipping%201%20billion%20cores.pdf#page=88.00">"How to Secure Unique EcosystemShipping 1 Billion+ Cores?"</a> <span class="cs1-format">(PDF)</span><span class="reference-accessdate">. Retrieved <span class="nowrap">13 August</span> 2025</span>.</cite><span class="cs1-maint citation-comment"><code class="cs1-code">{{cite web}}</code>: CS1 maint: url-status (link)</span></span>

</li>

<li id="cite_note-6"><span class="mw-cite-backlink"><b><a href="#cite_ref-6">^</a></b></span> <span class="reference-text"><cite class="citation web cs1"><a rel="nofollow" class="external text" href="https://github.com/rod-chapman/SPARKNaCl">"SPARKNaCl"</a>. <i><a href="GitHub" title="GitHub">GitHub</a></i>. 8 October 2021.</cite></span>

</li>

</ol></div></div>

<div class="mw-heading mw-heading2"><h2 id="Further_reading">Further reading</h2></div>

<ul><li><cite id="CITEREFBarnes2012" class="citation book cs1"><a href="John_Barnes_(computer_scientist)" title="John Barnes (computer scientist)">Barnes, John</a> (2012). <a rel="nofollow" class="external text" href="https://web.archive.org/web/20161014175327/http://www.cpibookdelivery.com/book/9780957290518/SPARK__The_Proven_Approach_to_High_Integrity_Software"><i>SPARK: The Proven Approach to High Integrity Software</i></a>. Altran Praxis. <a href="ISBN_(identifier)" class="mw-redirect" title="ISBN (identifier)">ISBN</a> <bdi>978-0-9572905-1-8</bdi>. Archived from <a rel="nofollow" class="external text" href="http://www.cpibookdelivery.com/book/9780957290518/SPARK__The_Proven_Approach_to_High_Integrity_Software">the original</a> on 14 October 2016<span class="reference-accessdate">. Retrieved <span class="nowrap">31 December</span> 2014</span>.</cite></li></ul>

<ul><li><cite id="CITEREFMcCormickChapin2015" class="citation book cs1">McCormick, John W.; Chapin, Peter C. (2015). <a rel="nofollow" class="external text" href="http://www.cambridge.org/9781107656840"><i>Building High Integrity Applications with SPARK</i></a>. Cambridge University Press. <a href="ISBN_(identifier)" class="mw-redirect" title="ISBN (identifier)">ISBN</a> <bdi>978-1-107-65684-0</bdi>.</cite></li></ul>

<ul><li><cite id="CITEREFRoss2005" class="citation journal cs1">Ross, Philip E. (September 2005). <span class="id-lock-subscription" title="Paid subscription required"><a rel="nofollow" class="external text" href="https://spectrum.ieee.org/the-exterminators">"The Exterminators"</a></span>. <i><a href="IEEE_Spectrum" title="IEEE Spectrum">IEEE Spectrum</a></i>. <b>42</b> (9): <span class="nowrap">36–</span>41. <a href="Doi_(identifier)" class="mw-redirect" title="Doi (identifier)">doi</a>:<a rel="nofollow" class="external text" href="https://doi.org/10.1109%2FMSPEC.2005.1502527">10.1109/MSPEC.2005.1502527</a>. <a href="ISSN_(identifier)" class="mw-redirect" title="ISSN (identifier)">ISSN</a> <a rel="nofollow" class="external text" href="https://search.worldcat.org/issn/0018-9235">0018-9235</a>. <a href="S2CID_(identifier)" class="mw-redirect" title="S2CID (identifier)">S2CID</a> <a rel="nofollow" class="external text" href="https://api.semanticscholar.org/CorpusID:26369398">26369398</a>.</cite></li></ul>

<div class="mw-heading mw-heading2"><h2 id="External_links">External links</h2></div>

<ul><li><a rel="nofollow" class="external text" href="http://www.spark-2014.org/">SPARK 2014 community site</a></li>

<li><a rel="nofollow" class="external text" href="http://www.adacore.com/sparkpro/">SPARK Pro website</a></li>

<li><a rel="nofollow" class="external text" href="http://libre.adacore.com/">SPARK Libre (GPL) Edition website</a> <a rel="nofollow" class="external text" href="https://web.archive.org/web/20050212023242/http://libre.adacore.com/">Archived</a> 12 February 2005 at the <a href="Wayback_Machine" title="Wayback Machine">Wayback Machine</a></li>

<li><a rel="nofollow" class="external text" href="http://www.altran.com/">Altran</a></li>

<li><a rel="nofollow" class="external text" href="http://www.crosstalkonline.org/storage/issue-archives/2005/200512/200512-Croxford.pdf">Correctness by Construction: A Manifesto for High-Integrity Software</a> <a rel="nofollow" class="external text" href="https://web.archive.org/web/20121030153055/http://www.crosstalkonline.org/storage/issue-archives/2005/200512/200512-Croxford.pdf">Archived</a> 30 October 2012 at the <a href="Wayback_Machine" title="Wayback Machine">Wayback Machine</a></li>

<li><a rel="nofollow" class="external text" href="http://www.safety-club.org.uk/">UK's Safety-Critical Systems Club</a></li>

<li><a rel="nofollow" class="external text" href="https://frama-c.com/html/fc-discuss/2009-November/msg00027.html">Comparison with a C specification language (Frama C)</a></li>

<li><a rel="nofollow" class="external text" href="http://www.adacore.com/tokeneer">Tokeneer Project Page</a></li>

<li><a rel="nofollow" class="external text" href="http://muen.codelabs.ch">Muen Kernel Public Release</a></li>

<li><a rel="nofollow" class="external text" href="http://lifeflow.mae.virginia.edu">LifeFlow LVAD Project</a></li>

<li><a rel="nofollow" class="external text" href="http://www.cubesatlab.org">VTU CubeSat Project</a></li></ul>

/* start https://en.wikipedia.org/ */

.mw-parser-output .hlist dl,.mw-parser-output .hlist ol,.mw-parser-output .hlist ul{margin:0;padding:0}.mw-parser-output .hlist dd,.mw-parser-output .hlist dt,.mw-parser-output .hlist li{margin:0;display:inline}.mw-parser-output .hlist.inline,.mw-parser-output .hlist.inline dl,.mw-parser-output .hlist.inline ol,.mw-parser-output .hlist.inline ul,.mw-parser-output .hlist dl dl,.mw-parser-output .hlist dl ol,.mw-parser-output .hlist dl ul,.mw-parser-output .hlist ol dl,.mw-parser-output .hlist ol ol,.mw-parser-output .hlist ol ul,.mw-parser-output .hlist ul dl,.mw-parser-output .hlist ul ol,.mw-parser-output .hlist ul ul{display:inline}.mw-parser-output .hlist .mw-empty-li{display:none}.mw-parser-output .hlist dt::after{content:": "}.mw-parser-output .hlist dd::after,.mw-parser-output .hlist li::after{content:" · ";font-weight:bold}.mw-parser-output .hlist dd:last-child::after,.mw-parser-output .hlist dt:last-child::after,.mw-parser-output .hlist li:last-child::after{content:none}.mw-parser-output .hlist dd dd:first-child::before,.mw-parser-output .hlist dd dt:first-child::before,.mw-parser-output .hlist dd li:first-child::before,.mw-parser-output .hlist dt dd:first-child::before,.mw-parser-output .hlist dt dt:first-child::before,.mw-parser-output .hlist dt li:first-child::before,.mw-parser-output .hlist li dd:first-child::before,.mw-parser-output .hlist li dt:first-child::before,.mw-parser-output .hlist li li:first-child::before{content:" (";font-weight:normal}.mw-parser-output .hlist dd dd:last-child::after,.mw-parser-output .hlist dd dt:last-child::after,.mw-parser-output .hlist dd li:last-child::after,.mw-parser-output .hlist dt dd:last-child::after,.mw-parser-output .hlist dt dt:last-child::after,.mw-parser-output .hlist dt li:last-child::after,.mw-parser-output .hlist li dd:last-child::after,.mw-parser-output .hlist li dt:last-child::after,.mw-parser-output .hlist li li:last-child::after{content:")";font-weight:normal}.mw-parser-output .hlist ol{counter-reset:listitem}.mw-parser-output .hlist ol>li{counter-increment:listitem}.mw-parser-output .hlist ol>li::before{content:" "counter(listitem)"\a0 "}.mw-parser-output .hlist dd ol>li:first-child::before,.mw-parser-output .hlist dt ol>li:first-child::before,.mw-parser-output .hlist li ol>li:first-child::before{content:" ("counter(listitem)"\a0 "}

/* end https://en.wikipedia.org/ */

</style><style data-mw-deduplicate="TemplateStyles:r1236075235">

/* start https://en.wikipedia.org/ */

.mw-parser-output .navbox{box-sizing:border-box;border:1px solid #a2a9b1;width:100%;clear:both;font-size:88%;text-align:center;padding:1px;margin:1em auto 0}.mw-parser-output .navbox .navbox{margin-top:0}.mw-parser-output .navbox+.navbox,.mw-parser-output .navbox+.navbox-styles+.navbox{margin-top:-1px}.mw-parser-output .navbox-inner,.mw-parser-output .navbox-subgroup{width:100%}.mw-parser-output .navbox-group,.mw-parser-output .navbox-title,.mw-parser-output .navbox-abovebelow{padding:0.25em 1em;line-height:1.5em;text-align:center}.mw-parser-output .navbox-group{white-space:nowrap;text-align:right}.mw-parser-output .navbox,.mw-parser-output .navbox-subgroup{background-color:#fdfdfd}.mw-parser-output .navbox-list{line-height:1.5em;border-color:#fdfdfd}.mw-parser-output .navbox-list-with-group{text-align:left;border-left-width:2px;border-left-style:solid}.mw-parser-output tr+tr>.navbox-abovebelow,.mw-parser-output tr+tr>.navbox-group,.mw-parser-output tr+tr>.navbox-image,.mw-parser-output tr+tr>.navbox-list{border-top:2px solid #fdfdfd}.mw-parser-output .navbox-title{background-color:#ccf}.mw-parser-output .navbox-abovebelow,.mw-parser-output .navbox-group,.mw-parser-output .navbox-subgroup .navbox-title{background-color:#ddf}.mw-parser-output .navbox-subgroup .navbox-group,.mw-parser-output .navbox-subgroup .navbox-abovebelow{background-color:#e6e6ff}.mw-parser-output .navbox-even{background-color:#f7f7f7}.mw-parser-output .navbox-odd{background-color:transparent}.mw-parser-output .navbox .hlist td dl,.mw-parser-output .navbox .hlist td ol,.mw-parser-output .navbox .hlist td ul,.mw-parser-output .navbox td.hlist dl,.mw-parser-output .navbox td.hlist ol,.mw-parser-output .navbox td.hlist ul{padding:0.125em 0}.mw-parser-output .navbox .navbar{display:block;font-size:100%}.mw-parser-output .navbox-title .navbar{float:left;text-align:left;margin-right:0.5em}body.skin--responsive .mw-parser-output .navbox-image img{max-width:none!important}@media print{body.ns-0 .mw-parser-output .navbox{display:none!important}}

/* end https://en.wikipedia.org/ */

</style></div><div role="navigation" class="navbox authority-control" aria-labelledby="Authority_control_databases_frameless&#124;text-top&#124;10px&#124;alt=Edit_this_at_Wikidata&#124;link=https&#58;//www.wikidata.org/wiki/Q3493345#identifiers&#124;class=noprint&#124;Edit_this_at_Wikidata647" style="padding:3px"><table class="nowraplinks hlist mw-collapsible autocollapse navbox-inner" style="border-spacing:0;background:transparent;color:inherit"><tbody><tr><th scope="col" class="navbox-title" colspan="2"><div id="Authority_control_databases_frameless&#124;text-top&#124;10px&#124;alt=Edit_this_at_Wikidata&#124;link=https&#58;//www.wikidata.org/wiki/Q3493345#identifiers&#124;class=noprint&#124;Edit_this_at_Wikidata647" style="font-size:114%;margin:0 4em">Authority control databases </div></th></tr><tr><th scope="row" class="navbox-group" style="width:1%">National</th><td class="navbox-list-with-group navbox-list navbox-odd" style="width:100%;padding:0"><div style="padding:0 0.25em"><ul><li><span class="uid"><a rel="nofollow" class="external text" href="https://id.loc.gov/authorities/sh2015001170">United States</a></span></li><li><span class="uid"><a rel="nofollow" class="external text" href="https://www.nli.org.il/en/authorities/987007411089005171">Israel</a></span></li></ul></div></td></tr><tr><th scope="row" class="navbox-group" style="width:1%">Other</th><td class="navbox-list-with-group navbox-list navbox-even" style="width:100%;padding:0"><div style="padding:0 0.25em"><ul><li><span class="uid"><a rel="nofollow" class="external text" href="https://lux.collections.yale.edu/view/concept/8541f691-077e-458f-b99b-33c1c676a5ec">Yale LUX</a></span></li></ul></div></td></tr></tbody></table></div></div><div><div class="zim-footer">

This article is issued from <a class="external text" title="Last edited on 2025-07-20" href="https://en.wikipedia.org/wiki/?title=SPARK_(programming_language)&oldid=1301469202">Wikipedia</a>. The text is available under <a class="external text" href="https://creativecommons.org/licenses/by-sa/4.0/deed.en">Creative Commons Attribution-Share Alike 4.0</a> unless otherwise noted. Additional terms may apply for the media files.

</div>

</div></div>

</div>

</main>

</div>

</body></html>